package fst.calculi.STLC

import fst.parsing._
import fst.binding.Binding
import fst.results.Results

trait Typers extends Results {
  val syntax: Syntax
  import syntax._
  
  type ErrorInfo = String
  type Info = Unit // info is not used here -- should track position of AST node that the result is associated to
  def chooseBestResult(a: NoSuccess, b: NoSuccess): NoSuccess = a
  
	def result[T](r: T): Success[T] = result((), r)
  def failure: Failure = failure(())
  def error: Error = error(())
	def result[T](in: Info, r: T): Success[T] = Success(r, in)(Failure("zero", in))
  def failure(in: Info): Failure = Failure("unknown failure", in)
  def error(in: Info): Error = Error("unknown error", in)
  

  object Typer {
    val empty: Typer = apply{name => failure explain("unbound name: "+name)}    
    def apply(f: Name => Result[Type]): Typer = new Typer { def apply(n: Name) = f(n) }
  }
  trait TyperCore extends (Name => Result[Type]) {
    def update(n: Name, tp: Type): Typer = Typer{name => if(name == n) result(tp) else this(name) }
  }

  trait Typer extends TyperCore {
    def typeOf(tm: Term): Result[Type] = tm match {
      case Var(n) => this(n)
      case Abs(from, \\(x, b)) => 
        for(to <- (this(x) = from).typeOf(b)) 
          yield TArr(from, to)
      case App(fun, arg) => 
        for(funTp <- typeOf(fun); 
            (from, to) <- isTArr(funTp);
            tpArg <- typeOf(arg); 
            _ <- isEqual(tpArg, from) explain("argument "+ arg.prettyPrint +" : "+ tpArg.prettyPrint +" cannot be passed to "+ fun.prettyPrint +" : "+ funTp.prettyPrint)) yield to
      case b if b eq LTrue => result(TBool)
      case b if b eq LFalse => result(TBool)
    }
  }
  
  def isEqual(tp1: Type, tp2: Type): Result[Unit] = if(tp1 == tp2) result(()) else failure
  def isTArr(tp: Type): Result[(Type, Type)] = tp match { 
    case TArr(from, to) => result((from, to)) 
    case _ => failure explain("expected function type, found: "+tp)
  }
  
  def typeOf(t: Term) = Typer.empty.typeOf(t)
}

object TyperTest extends Typers {
  object syntax extends Syntax
  
  val parser = new Parsing { val syntax = TyperTest.syntax }
  
  def main(args: Array[String]) = println(for(p <- parser.parse(args(0))) yield typeOf(p))
}